Problem with findMUS in 2.9.0

Mikael Zayenz Lagerkvist

unread,

Feb 28, 2025, 4:12:49 PMFeb 28

to MiniZinc

Hi,

I have a model that is unsatisfiable for a certain instance with both Gecode and OR-Tools. However, when I run findMUS, the only output I get is

Running model.mzn, medium-test.dzn

    % Generated FlatZinc statistics:
    %%%mzn-stat: paths=1266
    %%%mzn-stat: flatBoolVars=324
    %%%mzn-stat: flatIntVars=286
    %%%mzn-stat: flatBoolConstraints=216
    %%%mzn-stat: flatIntConstraints=461
    %%%mzn-stat: evaluatedReifiedConstraints=324
    %%%mzn-stat: method="minimize"
    %%%mzn-stat: flatTime=0.169678
    %%%mzn-stat-end
    SubSolver: hard cons: 385 soft cons: 292 leaves: 292 branches: 317 Built tree in 0.04656 seconds.
    MiniZinc:

Finished in 323msec.

When I make another model unsatisfiable, it gives me the right type of output telling me what (set of) constraints constitutes the error. What could be the reason for the above missing output from findMUS?

Cheers,

Mikael

kevin.k...@gmail.com

unread,

Mar 4, 2025, 6:12:14 AMMar 4

to MiniZinc

Hi Mikael,

The "MiniZinc:" bit looks like FindMUS was trying to output an exception from MiniZinc (probably from the solver since it looks like flattening has succeeded).

I'll have a look to see if there are Exceptions we aren't handling or of there was a change in how they are meant to be handled.

Do you have a minimal example you can share?

Regards,

Kevin

Mikael Zayenz Lagerkvist

unread,

Mar 4, 2025, 11:05:22 AMMar 4

to mini...@googlegroups.com

Hi kevin,

Thanks, that does explain a bit better what was happening.
Unfortunately, I don't have a small reproducing example. I will try to
make one that is sufficiently anonymized when I can, but it will take
some time.

I did find out later that one of the problems in the mus was a regular
over enums if that helps. I found that out by doing the traditional
method of commenting out constraints until I found the issue :-)

Cheers,
Mikael

> --
> You received this message because you are subscribed to the Google Groups "MiniZinc" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to minizinc+u...@googlegroups.com.
> To view this discussion visit https://groups.google.com/d/msgid/minizinc/e32e8b68-6b2e-47db-9766-187b27c48b23n%40googlegroups.com.

--
Mikael Zayenz Lagerkvist

kevin.k...@gmail.com

unread,

Mar 4, 2025, 1:10:21 PMMar 4

to MiniZinc

Actually the mention of regular reminded me that at some point there was an inconsistency between the stand alone and embedded versions of gecode (findMUS by default uses the embedded gecode_presolver solver).

Did you set the solver (with the --subsolver argument) when calling findMUS or leave it as the default?

Kevin

Mikael Zayenz Lagerkvist

unread,

Mar 4, 2025, 1:20:25 PMMar 4

to mini...@googlegroups.com, MiniZinc

Hi,

I ran it from the IDE and used all default settings. Version 2.9.0, with a regular constraint over enum variables with a textual regexp and due to 2.9.0 issues using enum2int for the variables.

Essentially, the problem was that I had an expression ”A* [^A]+ A*” and that be of the constraints was forced over a string of only A, which was the core of the issue.

Cheers

Mikael

On 4 Mar 2025, at 08:40, kevin.k...@gmail.com <kevin.k...@gmail.com> wrote:

To view this discussion visit https://groups.google.com/d/msgid/minizinc/ff2ff560-a62c-418d-9c0a-d44cdccaeacfn%40googlegroups.com.

Reply all

Reply to author

Forward